#!/bin/bash
# ulimit -v 4194304  # Set the virtual memory limit to 2GB
ulimit -v 8388608  # Set the virtual memory limit to 2GB

bench_dir=$2
exec_bin=$3
log_output_file_path=$4

function check_file_status {
    local filename="$1"

    # 检查文件内容
    if [[ "$filename" == *"dfaComb"* ]]; then
        if [[ "$filename" == *"m1"* ]]; then
            echo 2
        elif [[ "$filename" == *"m2"* ]]; then
            echo 3
        else
            echo "未找到m1或m2"
        fi
    else
        if [[ "$filename" == *"wholeDFA"* ]]; then
            echo 1
        else
            echo 0
        fi
    fi
}

executeCase() {
    local ltlf_file=$1
    local tlsf_file="${ltlf_file%.ltlf}.tlsf"
    local part_file="${ltlf_file%.ltlf}.var"
    if [ ! -e "$part_file" ]; then
        part_file="${ltlf_file%.ltlf}.part"
    fi
    local res_file="${ltlf_file%.ltlf}.res"
    local pbs_file="${ltlf_file%.ltlf}.pbs"
    local pbs_id="${ltlf_file%.ltlf}"

    set -x

    ltlf_file=$bench_dir/$ltlf_file
    tlsf_file=$bench_dir/$tlsf_file
    part_file=$bench_dir/$part_file
    res_file=$bench_dir/$res_file

    cd /public/home/jwli/workSpace/yongkang/qsub_trash
    exec_base=$(basename $exec_bin)

    # timeout_mins=5
    # timeout_mins=10
    timeout_mins=30
    timeout_secs=$((timeout_mins * 60 + 30))

    export TIME_LIMIT=$timeout_mins
    export SPDLOG_LEVEL=warn
    export SYN_IDX=$(check_file_status $exec_base)
    export EXPORT_DOTS=0

    # # no
    # export SAT_TRACE=$(grep -q "OneStep" "$exec_base" && echo 0 || echo 1)
    # export PRECHECK=$(grep -q "noPreCheck" "$exec_base" && echo 0 || echo 1)
    # # yes
    # export SORT_FLAG=$(grep -q "sort" "$exec_base" && echo 1 || echo 0)
    # export METHOD2_FLAG=$(grep -q "COMBINE02" "$exec_base" && echo 1 || echo 0)
    # export SPLIT_AND=$(grep -q "splitAnd" "$exec_base" && echo 1 || echo 0)
    # export SYS_GROUP=$(grep -q "sysGroup" "$exec_base" && echo 1 || echo 0)
    # if grep -q "level[0-9]" "$exec_base"; then
    #     export SYS_GROUP_LEVEL=$(grep -o "level[0-9]\+" "$exec_base" | sed 's/level//')
    #     echo "Found level: $SYS_GROUP_LEVEL"
    # # else
    # #     echo "No level found"
    # fi
    if [[ $exec_base == XXXX* ]]; then
        echo 'ERROR: just EMPTY placeholder' > $res_file
    elif [[ $exec_base == ltlfsyn_* ]]; then
        (/usr/bin/time -v timeout $timeout_secs $exec_bin $ltlf_file $part_file) &> $res_file
    elif [[ $exec_base == cynthia* ]]; then
        # cynthia
        # default location /public/home/jwli/workSpace/yongkang/23.0802/cynthia-app
        (/usr/bin/time -v timeout $timeout_secs $exec_bin -n -f $ltlf_file --part $part_file) &> $res_file
    elif [[ $exec_base == lisa_env_syntcomp* ]]; then
        # === MUST BEFORE others === #
        # lisa_env_syntcomp
        # /public/home/jwli/workSpace/yongkang/JACM-24March-labs/bins/lisasyntcomp/lisa_env_syntcomp_default.sh
        cd /public/home/jwli/workSpace/yongkang/JACM-24March-labs/bins/lisasyntcomp
        (/usr/bin/time -v timeout $timeout_secs ./starexec_run_seqreal1.sh $tlsf_file) &> $res_file
    elif [[ $exec_base == lisa_env* ]]; then
        # lisa_env
        # /public/home/jwli/workSpace/yongkang/23.0906/lisa_env-static
        export PATH=$PATH:/public/home/jwli/workSpace/yongkang/usr/bin
        export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:/public/home/jwli/workSpace/yongkang/usr/lib
        ( mkdir -p $PWD$ltlf_file ; cd $PWD$ltlf_file; time timeout $timeout_secs $exec_bin -syn -ltlf $ltlf_file -part $part_file) &> $res_file
    elif [[ $exec_base == lisa_sys* ]]; then
        # lisa
        # /public/home/jwli/workSpace/yongkang/23.0906/lisa_sys-static
        export PATH=$PATH:/public/home/jwli/workSpace/yongkang/usr/bin
        export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:/public/home/jwli/workSpace/yongkang/usr/lib
        (/usr/bin/time -v timeout $timeout_secs $exec_bin -syn -ltlf $ltlf_file -part $part_file) &> $res_file
    elif [[ $exec_base == lydia_env_syntcomp* ]]; then
        # === MUST BEFORE others === #
        # lydia_env_syntcomp
        # /public/home/jwli/workSpace/yongkang/JACM-24March-labs/bins/lydia_env_syntcomp_static
        ( cd /public/home/jwli/workSpace/yongkang/JACM-24March-labs/bins/ ; time timeout $timeout_secs $exec_bin -f $tlsf_file) &> $res_file
    elif [[ $exec_base == lydia_env* ]]; then
        # lydia_env
        # /public/home/jwli/workSpace/yongkang/23.0803/lydia_env
        (/usr/bin/time -v timeout $timeout_secs $exec_bin --env -n -l ltlf -f $ltlf_file --part $part_file) &> $res_file
    elif [[ $exec_base == lydia_sys* ]]; then
        # lydia
        # /public/home/jwli/workSpace/yongkang/23.0803/lydia_sys
        (/usr/bin/time -v timeout $timeout_secs $exec_bin -n -l ltlf -f $ltlf_file --part $part_file) &> $res_file
    elif [[ $exec_base == nike_env* ]]; then
        # nike
        # /public/home/jwli/workSpace/yongkang/JACM-24March-labs/bins/nike
        (time timeout $timeout_secs $exec_bin --no-empty --file $ltlf_file --part $part_file -m bdd -s random) &> $res_file
    else
        echo "no matched exec_bin type" >&2
    fi
}
executeCase $1
